FDL - Nuprl Lemma : write-restricted

Nuprl Lemma : write-restricted_wf

R:Realizer, k:Knd, i:Id. write-restricted(R;i;k)

Definitions	Realizer, t T, Knd, Id, type List, false, IdLnk, x:A. B(x), a = b, a = b, p q, Type, x. t(x), a:A fp B(a), Prop, x:AB(x), State(ds), DeclaredType(ds;x), x:AB(x), , p q, x,y,z. t(x;y;z), x,y,z,w,v. t(x;y;z;w;v), x,y,z,u,v,w. t(x;y;z;u;v;w), x,y,z,w. t(x;y;z;w), es realizer ind, write-restricted(R;i;k)
Lemmas	es realizer ind wf, bor wf, bool wf, decl-type wf, decl-state wf, fpf wf, band wf, eq id wf, eq knd wf, IdLnk wf, bfalse wf, Id wf, Knd wf, es realizer wf